#include"dpll.h"
#include"sse_avx.h"
//#include"timer.h"
//extern timer tm;
int CERR_LEVEL;
extern long long threshold;
_bool dpll_satisfiable(cnf*_cnf){
    printf("start \n");
    dpllresult* result = DPLLalgorithm(_cnf);
    _cnf = new_cnf_from(result->model_cnf);
    print_cnf(_cnf);
    printf("%p\n", _cnf);
    return result->sat;
}

variable* find_first_unassigned(variable* vars, int nvar){
#ifdef __vector
    __m128i assignmask, iter, testbit;
    variable test[4];
    unsigned int test4[4];
    assignmask = _mm_set_epi32(0x00040000,0x00040000,0x00040000,0x00040000);
    int i;
    for(i = 0; i < nvar-4; i+=4){
        iter = _mm_loadu_si128((void*)&vars[i]);

        iter = _mm_and_si128(iter, assignmask);
        testbit = _mm_cmpeq_epi32(iter, assignmask);
        // _mm_store_si128((void*)&test[0], testbit);
        // for(int j = 0; j < 4; j++){
        //     printf("name %d ,flag %d\n", test[j].name, test[j].flag);
        // }
        if(_mm_test_all_ones(testbit)) continue;
        _mm_store_si128((void*)&test4[0], testbit);
        for(int j = 0; j < 4; j++){
            if (test4[j] == 0x00000000){
                return &vars[i+j];
            }
        }
        assert(0);//shouldn't reach here;
    }
    for(; i < nvar; i++){
        if (!get_vflag(&vars[i], assigned)){
            return &vars[i];
        }
    }   
#endif
#ifdef __serial
    for(int i = 0; i < nvar; i++){
        if (!get_vflag(&vars[i], assigned)){
            return &vars[i];
        }
    }   
#endif
    return NULL;
}

/**
 * Checks if all clauses are true
 */
_bool ALL_CLAUSES_ARE_TRUE(clause* cls_set, int ncls){
    for(int i = 0; i < ncls; i++){
        //if (cls_set[i].true_val_available && cls_set[i].true_val) continue;
        if (!clause_is_true(&cls_set[i])){
            return false;
        }
    }
    // for(int i = 0; i < ncls; i++){
    //     //printf("#%d ", i);
    //     print_clause(&cls_set[i]);
    // }
    printf("ALL_CLAUSES_ARE_TRUE %p\n", cls_set);
    return true;
}

_bool ONE_CLAUSE_IS_FALSE(clause* cls_set, int ncls){
    for(int i = 0; i < ncls; i++){
        if (clause_is_false(&cls_set[i])){
            //printf("false clause is %d:\n", i);
            assert(cls_set[i].var_num > 0);
            //print_clause(&cls_set[i]);
            return true;
        }
    }
    return false;
}

variable* FIND_UNIT_CLAUSE(cnf* cnf){
    clause* cls = NULL;
    for(int i = 0; i < cnf->nclause; i++){
        cls = &cnf->clause_set[i];
        if(!clause_is_true(cls)){
            int count = cls->var_num;
            variable*unasigned = NULL;
            //在3sat问题中，这个不适合vectorize，因为都是3个variable
            for(int j = 0; j < cls->var_num; j++){
                if(get_vflag(&cls->vars[j], assigned)){
                    count--;
                }
                else{
                    unasigned = &cls->vars[j];
                }
            }
            if (count == 1) {
                return unasigned;
            }
        }
    }
    return NULL;
}

unit_pair* FIND_UNIT_CLAUSE_P(cnf* cnf, _bool seq){
    clause* cls = NULL;
    if (seq > 0){
        for(int i = 0; i < cnf->nclause; i++){
            cls = &cnf->clause_set[i];
            if(!clause_is_true(cls)){
                int count = cls->var_num;
                variable*unasigned = NULL;
                //在3sat问题中，这个不适合vectorize，因为都是3个variable
                for(int j = 0; j < cls->var_num; j++){
                    if(get_vflag(&cls->vars[j], assigned)){
                        count--;
                    }
                    else{
                        unasigned = &cls->vars[j];
                    }
                }
                if (count == 1) {
                    unit_pair* ret = malloc(sizeof(unit_pair));
                    ret->cls = cls;
                    ret->var = unasigned;
                    assert(cls != NULL && unasigned != NULL);
                    return ret;
                }
            }
        }    
    }
    else{
        for(int i = cnf->nclause-1; i >= 0; i--){
            cls = &cnf->clause_set[i];
            if(!clause_is_true(cls)){
                int count = cls->var_num;
                variable*unasigned = NULL;
                //在3sat问题中，这个不适合vectorize，因为都是3个variable
                for(int j = 0; j < cls->var_num; j++){
                    if(get_vflag(&cls->vars[j], assigned)){
                        count--;
                    }
                    else{
                        unasigned = &cls->vars[j];
                    }
                }
                if (count == 1) {
                    unit_pair* ret = malloc(sizeof(unit_pair));
                    ret->cls = cls;
                    ret->var = unasigned;
                    assert(cls != NULL && unasigned != NULL);
                    return ret;
                }
            }
        }
    }

    //printf("pair is NULL\n");
    return NULL;
}


void set_variable_value(cnf* cnf, variable* var, _bool value){
    assert(sizeof(variable) == sizeof(int));//security check
    int name = var->name;
#ifdef __serial
    for(int i = 0; i < cnf->nvar; i++){
        if(name == cnf->vars[i].name){
            cnf->vars[i].assigned = true;
            cnf->vars[i].value = value;
            //printf("index %d, set flag to %d\n", i,  cnf->vars[i].flag);
        }
    }
    for(int i = 0; i < cnf->n_univar; i++){
        if(name == cnf->var_set[i].name){
            cnf->var_set[i].assigned = true;
            cnf->var_set[i].value = value;
        }
    }
#endif 
#ifdef __vector
    //printf("look for name %d\n", name);
    //printf("sizeof varaible %d %d %d\n", (int)sizeof(variable), (int)sizeof(short), (int)sizeof(__uint16_t));
    
    __m128i namemask, nameiter, nameiter2, namemask2, flagsetmask;
    if(value){
        //[assign, value, sign]
        flagsetmask = _mm_set_epi32(0x00060000, 0x00060000, 0x00060000, 0x00060000);
    }
    else{
        flagsetmask = _mm_set_epi32(0x00040000, 0x00040000, 0x00040000, 0x00040000);
    }
    namemask = _mm_set_epi32(0x0000FFFF, 0x0000FFFF, 0x0000FFFF, 0x0000FFFF);
    namemask2 = _mm_set_epi32(name, name, name, name);
    for(int i = 0; i < cnf->nvar; i+=4){
        nameiter = _mm_loadu_si128((void*)&cnf->vars[i]);
        // variable test[4];
        // _mm_store_si128((void*)&test[0], nameiter);
        // for(int j = 0; j < 4; j++){
        //     printf("name %d ,flag %d\n", test[j].name, test[j].flag);
        // }
        nameiter2 = _mm_and_si128(nameiter, namemask);
        // _mm_store_si128((void*)&test[0], nameiter2);
        // for(int j = 0; j < 4; j++){
        //     printf("name %d ,flag %d\n", test[j].name, test[j].flag);
        // }
        nameiter2 = _mm_cmpeq_epi32(nameiter2, namemask2);
        // _mm_store_si128((void*)&test[0], nameiter2);
        // for(int j = 0; j < 4; j++){
        //     printf("name %d ,flag %d\n", test[j].name, test[j].flag);
        // }
        nameiter2 = _mm_and_si128(nameiter2, flagsetmask);
        nameiter = _mm_or_si128(nameiter, nameiter2);
        // _mm_store_si128((void*)&test[0], nameiter);       
        // for(int j = 0; j < 4; j++){
        //     printf("name %d ,sign %d, value %d, assigned %d\n", 
        //     test[j].name, test[j].sign, test[j].value, test[j].assigned);
        // }
        // for(int j = 0; j < 4; j++){
        //     assert(test[j].flag == cnf->vars[i+j].flag);
        // }
        _mm_storeu_si128((void*)&cnf->vars[i], nameiter); //load back
    }
#endif
}


void unset_variable_value(cnf* cnf, variable* var){
    int name = var->name;
#ifdef __serial
    for(int i = 0; i < cnf->nvar; i++){
        if(name == cnf->vars[i].name){
            cnf->vars[i].assigned = false;
        }
    }
    for(int i = 0; i < cnf->n_univar; i++){
        if(name == cnf->var_set[i].name){
            cnf->var_set[i].assigned = false;            
        }
    }
#endif
#ifdef __vector
    TODO();
#endif 
}

variable* FIND_PURE_VAR(cnf* cnf){
    for(int i = 0; i < cnf->n_univar; i++){
        _bool occurred_positively = false;
        _bool occurred_negatively = false;
        clause* cls = NULL;
        variable* var;
        for(int c = 0; c < cnf->nclause; c++){
            cls = &cnf->clause_set[c];
            if(!clause_is_true(cls)){
                for(int j = 0; j < cls->var_num; j++){
                    if (cnf->var_set[i].name == cls->vars[j].name){
                        var = &cls->vars[j];
                        if (!get_vflag(&cls->vars[j], assigned) &&
                        !get_vflag(&cls->vars[j], sign)){
                            occurred_negatively = true; 
                        }
                        else if (!get_vflag(&cls->vars[j], assigned) &&
                        get_vflag(&cls->vars[j], sign)){
                            occurred_positively = true;
                        }    
                    }
                    if (occurred_positively && occurred_negatively) {
                        var = NULL;
                        break;
                    }
                }
            }            
        }
        //found pure
        if (!occurred_positively && occurred_negatively) {
            assert(var != NULL);
            return var;
        }
        else if(occurred_positively && !occurred_negatively){
            assert(var != NULL);
            return var;//&cnf->var_set[i];
        }
    }
    return NULL;
}

void set_variable_value_debug(const cnf* oldcnf, cnf* modifycnf, variable* var, int value){
    int name = var->name;
#ifdef __serial
    for(int i = 0; i < modifycnf->nvar; i++){
        //printf("i %d\n", i);
        if(name == modifycnf->vars[i].name){
            modifycnf->vars[i].assigned = true;
            assert((void*)&oldcnf->vars[i] != (void*)&modifycnf->vars[i]);
            modifycnf->vars[i].value = value;
        }
    }
#endif 
#ifdef __vector
    TODO();
#endif
    printf("ok\n");
}
dpllresult* branch_on_variable(variable* var, cnf* oldcnf){
    threshold++;
    if (CERR_LEVEL >= 1){
        //printf("dppl branch on %d \n", var->name);
    }
    _bool solve_locally = true;
    if (solve_locally){
        //if use dpll
        if (1){
            //print_cnf(oldcnf);
            cnf* copycnf = new_cnf_from(oldcnf);
            set_variable_value(copycnf, var, true);
            CERR_LEVEL++;
            dpllresult* result = DPLLalgorithm(copycnf);
            CERR_LEVEL--;
            if (result->sat){
                return result;
            }
            else{
                //printf("try to set var:%d false\n", var->name);
                delete_cnf(copycnf);
                set_variable_value(oldcnf, var, false);
                //print_cnf(oldcnf);
                CERR_LEVEL++;
                result =  DPLLalgorithm(oldcnf);
                CERR_LEVEL--;
                return result;
            }
        }else{
            TODO();
        }
    }
    else{
        TODO();
    }
    return NULL;
}
dpllresult res;
dpllresult* DPLLalgorithm(cnf* cnf){

    //printf("\ncurrent level %d, cnf addr %p\n", CERR_LEVEL, (void*)cnf);
    variable* var;
    if (CERR_LEVEL >= 3){
        //print_cnf(cnf);
    }
    
    // Is the formula sat for the given partial model?
    if(ALL_CLAUSES_ARE_TRUE(cnf->clause_set, cnf->nclause)){
        res.sat = true;
        res.model_cnf = cnf;
        return &res;
    }

    // Is the formula unsatisfiable for the given partial model?
    if(ONE_CLAUSE_IS_FALSE(cnf->clause_set, cnf->nclause)){
        //printf("conflict happend\n");
        res.sat = false;
        res.model_cnf = cnf;
        return &res;
    }

    // Pure literal rule
    var = FIND_PURE_VAR(cnf);
    if (var != NULL){
        //printf("pure rule on %d, set to %d\n", var->name, var->sign);
        set_variable_value(cnf, var, var->sign);
        return DPLLalgorithm(cnf);
    }

    // Unit clause rule
    var = FIND_UNIT_CLAUSE(cnf);
    if (var != NULL){
        set_variable_value(cnf, var, var->sign);
        //if (CERR_LEVEL >= 2){
        //printf("unit rule on %d\n", var->name);
        //}
        //if (CERR_LEVEL >= 3){
            //print_cnf(cnf);
        //}
        return DPLLalgorithm(cnf);
    }

    // branch on first unassigned variable
    var = find_first_unassigned(cnf->vars, cnf->nvar);
    //printf("dpll found unassigned %d var\n", var->name);
    if(var == NULL){
        res.model_cnf = NULL;
        res.sat = false;
        //CERR_LEVEL = 0;
        return &res;
    }
    else{
        return branch_on_variable(var, cnf);
    }
}
